Symbolic Liveness Analysis.md

Detects liveness violations (e.g. infinite loops)

Name:

Symbolic Liveness Analysis

Application domain/field:

Liveness properties Symbolic execution Bug detection

Type of tool (e.g. model checker, test generator):

Bug detector for liveness properties

Expected input thing:

?

Expected input format:

?

Expected output:

?

Internals (tools used, frameworks, techniques, paradigms, ...):

Symbolic Liveness Analysis was implemented as an extension of KLEE. It uses Z3.

Comments:

URIs (github, websites, etc.):

Repository: https://github.com/COMSYS/SymbolicLivenessAnalysis

Last commit date:

15 Dec 2021 (default branch) 16 Dec 2021 (last activity)

Last publication date:

18 July 2018

List of related papers:

https://doi.org/10.1007/978-3-319-96142-2_27 (CAV '18)

Related tools (tools mentioned or compared to in the paper):

Meta

:: PV4 :: detects liveness violations